Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	a__app(nil,YS)	→ mark(YS)
2:	a__app(cons(X,XS),YS)	→ cons(mark(X),app(XS,YS))
3:	a__from(X)	→ cons(mark(X),from(s(X)))
4:	a__zWadr(nil,YS)	→ nil
5:	a__zWadr(XS,nil)	→ nil
6:	a__zWadr(cons(X,XS),cons(Y,YS))	→ cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))
7:	a__prefix(L)	→ cons(nil,zWadr(L,prefix(L)))
8:	mark(app(X1,X2))	→ a__app(mark(X1),mark(X2))
9:	mark(from(X))	→ a__from(mark(X))
10:	mark(zWadr(X1,X2))	→ a__zWadr(mark(X1),mark(X2))
11:	mark(prefix(X))	→ a__prefix(mark(X))
12:	mark(nil)	→ nil
13:	mark(cons(X1,X2))	→ cons(mark(X1),X2)
14:	mark(s(X))	→ s(mark(X))
15:	a__app(X1,X2)	→ app(X1,X2)
16:	a__from(X)	→ from(X)
17:	a__zWadr(X1,X2)	→ zWadr(X1,X2)
18:	a__prefix(X)	→ prefix(X)

There are 18 dependency pairs:


19:	A__APP(nil,YS)	→ MARK(YS)
20:	A__APP(cons(X,XS),YS)	→ MARK(X)
21:	A__FROM(X)	→ MARK(X)
22:	A__ZWADR(cons(X,XS),cons(Y,YS))	→ A__APP(mark(Y),cons(mark(X),nil))
23:	A__ZWADR(cons(X,XS),cons(Y,YS))	→ MARK(Y)
24:	A__ZWADR(cons(X,XS),cons(Y,YS))	→ MARK(X)
25:	MARK(app(X1,X2))	→ A__APP(mark(X1),mark(X2))
26:	MARK(app(X1,X2))	→ MARK(X1)
27:	MARK(app(X1,X2))	→ MARK(X2)
28:	MARK(from(X))	→ A__FROM(mark(X))
29:	MARK(from(X))	→ MARK(X)
30:	MARK(zWadr(X1,X2))	→ A__ZWADR(mark(X1),mark(X2))
31:	MARK(zWadr(X1,X2))	→ MARK(X1)
32:	MARK(zWadr(X1,X2))	→ MARK(X2)
33:	MARK(prefix(X))	→ A__PREFIX(mark(X))
34:	MARK(prefix(X))	→ MARK(X)
35:	MARK(cons(X1,X2))	→ MARK(X1)
36:	MARK(s(X))	→ MARK(X)

The approximated dependency graph contains one SCC: {19-32,34-36}.

Consider the SCC {19-32,34-36}. By taking the AF π with π(a__from) = π(A__FROM) = π(cons) = π(from) = π(mark) = π(MARK) = π(s) = 1 together with the lexicographic path order with precedence a__prefix ≻ nil, a__zWadr ≻ a__app ≻ A__APP, a__zWadr ≻ A__ZWADR ≻ A__APP, a__app ≈ app, a__zWadr ≈ zWadr and a__prefix ≈ prefix, the rules in {3,8-18,21,28,29,35,36} are weakly decreasing and the rules in {1,2,4-7,19,20,22-27,30-32,34} are strictly decreasing. There is one new SCC.
- Consider the SCC {21,28,29,35,36}. By taking the AF π with π(a__from) = π(A__FROM) = π(cons) = π(from) = π(mark) = π(MARK) = 1 and π(a__prefix) = π(prefix) = [ ] together with the lexicographic path order with precedence a__prefix ≻ nil, a__zWadr ≻ a__app, a__app ≈ app, a__zWadr ≈ zWadr and a__prefix ≈ prefix, the rules in {3,8-18,21,28,29,35} are weakly decreasing and the rules in {1,2,4-7,36} are strictly decreasing. There is one new SCC.
  - Consider the SCC {21,28,29,35}. By taking the AF π with π(A__FROM) = π(cons) = π(mark) = π(MARK) = π(s) = 1 and π(a__prefix) = π(prefix) = [ ] together with the lexicographic path order with precedence a__prefix ≻ nil, a__zWadr ≻ a__app, a__app ≈ app, a__from ≈ from, a__zWadr ≈ zWadr and a__prefix ≈ prefix, the rules in {8-18,21,35} are weakly decreasing and the rules in {1-7,28,29} are strictly decreasing. There is one new SCC.
    - Consider the SCC {35}. There are no usable rules. By taking the AF π with π(MARK) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 35 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (58.71 seconds) --- May 4, 2006